6 people like it.
Like the snippet!

phantom types for dependent types; sized list; less than

Using phantom types to emulate simple dependent types and sized list. Inspired by: https://www.seas.upenn.edu/~sweirich/cis670/09/

 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
 7: 
 8: 
 9: 
10: 
11: 
12:

type Z = struct end
type S<'n> = struct end

type List<'n,'b> = L of 'b list
let nil : List<Z, 'b> = L []
let cons (b:'b) ((L bs) : List<'n, 'b>) : List<S<'n>,'b> = L (b::bs)

[<EntryPoint>]
let main args =
  let l3 : List<S<S<S<Z>>>,int> = cons 1 (cons 2 (cons 3 nil))
  printfn "%A; %A" l3 (cons 3 nil)
  0

type Z

type S<'n>

Multiple items
module List

from Microsoft.FSharp.Collections

--------------------
type List<'T> =
  | ( [] )
  | ( :: ) of Head: 'T * Tail: 'T list
    interface IReadOnlyList<'T>
    interface IReadOnlyCollection<'T>
    interface IEnumerable
    interface IEnumerable<'T>
    member GetReverseIndex : rank:int * offset:int -> int
    member GetSlice : startIndex:int option * endIndex:int option -> 'T list
    member Head : 'T
    member IsEmpty : bool
    member Item : index:int -> 'T with get
    member Length : int
    ...

--------------------
type List<'n,'b> = | L of 'b list

union case List.L: 'b list -> List<'n,'b>

type 'T list = List<'T>

val nil : List<Z,'b>

val cons : b:'b -> List<'n,'b> -> List<S<'n>,'b>

val b : 'b

val bs : 'b list

Multiple items
type EntryPointAttribute =
inherit Attribute
new : unit -> EntryPointAttribute

--------------------
new : unit -> EntryPointAttribute

val main : args:string [] -> int

val args : string []

val l3 : List<S<S<S<Z>>>,int>

Multiple items
val int : value:'T -> int (requires member op_Explicit)

--------------------
type int = int32

--------------------
type int<'Measure> = int

val printfn : format:Printf.TextWriterFormat<'T> -> 'T

Next Version Raw view Test code New version

More information

Link:	http://fssnip.net/7YI
Posted:	4 years ago
Author:	Vankata
Tags:	list , phantom types , #dependent types , playing with types , types